Communicating sequential processes

In computer science, communicating sequential processes (CSP) is a formal language for describing patterns of interaction in concurrent systems.^[1] It is a member of the family of mathematical theories of concurrency known as process algebras, or process calculi, based on message passing via channels. CSP was highly influential in the design of the occam programming language^[1]^[2] and also influenced the design of programming languages such as Limbo,^[3] RaftLib, Erlang,^[4] Go,^[5]^[3] Crystal, and Clojure's core.async.^[6]

CSP was first described in a 1978 article by Tony Hoare,^[7] but has since evolved substantially.^[8] CSP has been practically applied in industry as a tool for specifying and verifying the concurrent aspects of a variety of different systems, such as the T9000 Transputer,^[9] as well as a secure e-commerce system.^[10] The theory of CSP itself is also still the subject of active research, including work to increase its range of practical applicability (e.g., increasing the scale of the systems that can be tractably analyzed).^[11]

^ ^a ^b Roscoe, A. W. (1997). The Theory and Practice of Concurrency (PDF). Prentice Hall. ISBN 978-0-13-674409-2.
^ Inmos (1995-05-12). occam 2.1 Reference Manual (PDF). SGS-Thomson Microelectronics Ltd., INMOS document 72 occ 45 03.
^ ^a ^b Cox, Russ. "Bell Labs and CSP Threads". Retrieved 2010-04-15.
^ "10 Academic and Historical Questions". Retrieved 2021-11-15.
^ "FAQ: Why build concurrency on the ideas of CSP?". The Go Programming Language. Retrieved 2021-10-15.
^ Hickey, Rich (2013-06-28). "Clojure core.async Channels". Retrieved 2021-10-15.
^ Hoare, C. A. R. (1978). "Communicating sequential processes". Communications of the ACM. 21 (8): 666–677. doi:10.1145/359576.359585. S2CID 849342.
^ Abdallah, Ali E.; Jones, Cliff B.; Sanders, Jeff W. (2005). Communicating Sequential Processes: The First 25 Years. LNCS. Vol. 3525. Springer. ISBN 9783540258131.
^ Barrett, G. (1995). "Model checking in practice: The T9000 Virtual Channel Processor". IEEE Transactions on Software Engineering. 21 (2): 69–78. doi:10.1109/32.345823.
^ Hall, A; Chapman, R. (2002). "Correctness by construction: Developing a commercial secure system" (PDF). IEEE Software. 19 (1): 18–25. CiteSeerX 10.1.1.16.1811. doi:10.1109/52.976937.
^ Creese, S. (2001). Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks (D. Phil.). Oxford University. CiteSeerX 10.1.1.13.7185.

[roscoe-1] Roscoe, A. W. (1997). The Theory and Practice of Concurrency (PDF). Prentice Hall. ISBN 978-0-13-674409-2.

[2] Inmos (1995-05-12). occam 2.1 Reference Manual (PDF). SGS-Thomson Microelectronics Ltd., INMOS document 72 occ 45 03.

[cox-3] Cox, Russ. "Bell Labs and CSP Threads". Retrieved 2010-04-15.

[4] "10 Academic and Historical Questions". Retrieved 2021-11-15.

[golang-5] "FAQ: Why build concurrency on the ideas of CSP?". The Go Programming Language. Retrieved 2021-10-15.

[clojure-core-async-6] Hickey, Rich (2013-06-28). "Clojure core.async Channels". Retrieved 2021-10-15.

[hoare1978-7] Hoare, C. A. R. (1978). "Communicating sequential processes". Communications of the ACM. 21 (8): 666–677. doi:10.1145/359576.359585. S2CID 849342.

[25years-8] Abdallah, Ali E.; Jones, Cliff B.; Sanders, Jeff W. (2005). Communicating Sequential Processes: The First 25 Years. LNCS. Vol. 3525. Springer. ISBN 9783540258131.

[barrett-9] Barrett, G. (1995). "Model checking in practice: The T9000 Virtual Channel Processor". IEEE Transactions on Software Engineering. 21 (2): 69–78. doi:10.1109/32.345823.

[hall-10] Hall, A; Chapman, R. (2002). "Correctness by construction: Developing a commercial secure system" (PDF). IEEE Software. 19 (1): 18–25. CiteSeerX 10.1.1.16.1811. doi:10.1109/52.976937.

[11] Creese, S. (2001). Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks (D. Phil.). Oxford University. CiteSeerX 10.1.1.13.7185.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]